$\forall$$T$:Type, $L_{1}$, $L_{2}$:$T$ List, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$). sublist\_occurence($T$;$L_{1}$;$L_{2}$;$f$) $\in$ Prop